fetch airpo4.ax;

∀e walk home desk car S0;
∀e drive county home airport walk(car,S0);
∀e attrans1 I car airport drive(airport,walk(car S0));
tauteq 1:#2#2 1 walkable at1 at2 at3;
∀e ↑ car home;
tauteq 2:#2#2 2 drivable at4 at5 5 at3 notI 1 walkable at1 at2;
∀e ↑ I car;
tauteq 3:#2 1:7 at1 at2 at3 at4 at5 notI drivable walkable;

show proof→airpo4.prf;